es:ES, Sys:AbsInterface(Top), chain:(E(Sys)(Id List)).
chain-config(es;Sys;chain)  chain-config(es;Sys;(l.rev(l)) o chain) 

latex

Up	abstract chain replication
Definitions	ES, x:AB(x), P  Q, AbsInterface(A), Id, type List, E(X), f(a), rev(as), L1  L2, (e <loc e'), x:A. B(x), t  T, no_repeats(T;l), P  Q, x:A  B(x), P & Q, P  Q, left + right, P  Q, (x  l), loc(e), a < b, ||as||, #$n, s = t, x.A(x), f o g, chain-config(es;Sys;chain), Top, strong-subtype(A;B), s ~ t, b, E, {x:A| B(x)} , let x,y = A in B(x;y), t.1, a:A fp B(a), x:A. B(x), False, A, Atom$n, increasing(f;k), {T}, e < e', <a, b>, (e < e'), Type
Lemmas	reverse wf, sublist-reverse, member-reverse, es-loc wf, member wf, es-E wf, subtype rel wf, length-reverse, chain-config wf, es-interface wf, top wf, event system wf, no repeats wf, no repeats reverse, l member wf, Id wf, sublist wf, es-locl wf, es-E-interface wf